es:ES, X:AbsInterface(Top), e:E.
((e  le(X)))
 (le(X)(e) loc e 
 & ((le(X)(e)  X))
 & (e'':E. e'' loc e   (le(X)(e) <loc e'')  (((e''  X))))) 

latex

Definitions	x:AB(x), x:A. B(x), b, x:A  B(x), P & Q, P  Q, P  Q, t  T, s = t, Top, E, ES, AbsInterface(A), le(X), E(X), e  X, x.A(x)
Lemmas	assert wf, es-E-interface wf, es-le-interface wf, es-interface wf, event system wf, es-local-le-pred-property, es-E wf, top wf, es-is-interface wf